Micron Document
<!DOCTYPE html>
<html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-0 vector-toc-not-available vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-0 skin-theme-clientpref-day vector-sticky-header-enabled" lang="de" dir="ltr"><head>
<meta charset="UTF-8">
<title>Resolution (Logik)</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="icon" type="image/png" href="./_res_/favicon.png">
<link rel="canonical" href="https://de.wikipedia.org/wiki/Resolution_(Logik)"> <link href="./_mw_/ext.cite.styles.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.math.styles.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.wikimediamessages.styles.css" rel="stylesheet" type="text/css">
<link href="./_mw_/skins.vector.icons.css" rel="stylesheet" type="text/css">
<link href="./_mw_/skins.vector.search.codex.styles.css" rel="stylesheet" type="text/css">
<link href="./_mw_/skins.vector.styles.css" rel="stylesheet" type="text/css">
<meta name="ResourceLoaderDynamicStyles" content="">
<link href="./_mw_/ext.gadget.citeRef.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.defaultPlainlinks.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.dewikiCommonHide.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.dewikiCommonLayout.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.dewikiCommonStyle.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.dewikiDarkmode.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.dewikiResponsive.css" rel="stylesheet" type="text/css">
<link href="./_mw_/ext.gadget.specialSearch.css" rel="stylesheet" type="text/css">
<link rel="stylesheet" type="text/css" href="./_mw_/site.styles.css">
<link rel="stylesheet" type="text/css" href="./_mw_/noscript.css">
<link rel="stylesheet" type="text/css" href="./_res_/footer.css">
<link rel="stylesheet" type="text/css" href="./_res_/vector-2022.css">
</head>
<body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject page-Resolution_Logik rootpage-Resolution_Logik skin-vector-2022 action-view">
<div class="mw-page-container">
<div class="mw-page-container-inner">
<div class="mw-content-container">
<main id="content" class="mw-body">
<header class="mw-body-header vector-page-titlebar">
<h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Resolution (Logik)</span></h1>
</header>
<a id="top"></a>
<div id="bodyContent" class="vector-body ve-init-mw-desktopArticleTarget-targetContainer" aria-labelledby="firstHeading" data-mw-ve-target-container="">
<div id="contentSub">
<div id="mw-content-subtitle"></div>
</div>
<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="de" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="de" dir="ltr"><p>Die <b>Resolution</b> ist ein Verfahren der <a href="Formale_Logik" title="Formale Logik">formalen Logik</a>, um eine logische <a href="Formel" title="Formel">Formel</a> auf Gültigkeit zu testen.
</p><p>Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein <a href="Reductio_ad_absurdum" title="Reductio ad absurdum">Widerlegungsverfahren</a>: Statt direkt die <a href="Tautologie_(Logik)" title="Tautologie (Logik)">Allgemeingültigkeit</a> einer Formel zu zeigen, leitet es einen logischen Widerspruch aus deren Verneinung ab.
</p><p>Diese Herleitung geschieht mittels eines <a href="Algorithmus" title="Algorithmus">Algorithmus</a> auf rein formalem Weg und kann deshalb von einem Computerprogramm durchgeführt werden. Die Resolution ist eine der bekanntesten Techniken des <a href="Maschinengest%C3%BCtztes_Beweisen" title="Maschinengestütztes Beweisen">Maschinengestützten Beweisens</a>.
</p>

<div class="mw-heading mw-heading2"><h2 id="Das_Resolutionsverfahren_in_der_Aussagenlogik">Das Resolutionsverfahren in der Aussagenlogik</h2></div>
<div class="mw-heading mw-heading3"><h3 id="Resolvente_(auch:_Resolvent)"><span id="Resolvente_.28auch:_Resolvent.29"></span>Resolvente (auch: Resolvent)</h3></div>
<p>Seien <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/babf569931f1a7b5182b9bec51873c2f5692fbb8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{1}}" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/7ec545f7870665e1028b7492746848d149878808.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{2}}" loading="lazy"></span> <a href="Disjunktionsterm" title="Disjunktionsterm">Klauseln</a> einer <a href="Aussagenlogik" title="Aussagenlogik">aussagenlogischen</a> Formel, die in <a href="Konjunktive_Normalform" title="Konjunktive Normalform">konjunktiver Normalform</a> vorliegt. Gibt es ein <a href="Literal" title="Literal">Literal</a> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span>, welches in <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/babf569931f1a7b5182b9bec51873c2f5692fbb8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{1}}" loading="lazy"></span> positiv und in <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/7ec545f7870665e1028b7492746848d149878808.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{2}}" loading="lazy"></span> negativ vorkommt, ist die Vereinigung beider Klauseln ohne das positive und negative Literal <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span> eine Resolvente (auch: der Resolvent) <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{R}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{R}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/05366cec35ae08b2e88c7c1ce8dcba451d837959.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.141ex; height:2.509ex;" alt="{\displaystyle C_{R}}" loading="lazy"></span>. Das heißt insbesondere: Gibt es <b>kein</b> komplementäres Literal, so gibt es auch keine Resolvente.
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L\in C_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L\in C_{1}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/aa6e5442d077de6aae36de1efa84174c8038e09f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:7.14ex; height:2.509ex;" alt="{\displaystyle L\in C_{1}}" loading="lazy"></span></dd>
<dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\overline {L}}\in C_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>L</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\overline {L}}\in C_{2}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/37358e4175844bca60d4c7a5484c78116070d71c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:7.255ex; height:3.343ex;" alt="{\displaystyle {\overline {L}}\in C_{2}}" loading="lazy"></span></dd></dl>
<p><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msub>
<mo>=</mo>
<mo stretchy="false">(</mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo class="MJX-variant">∖<!-- ∖ --></mo>
<mo fence="false" stretchy="false">{</mo>
<mi>L</mi>
<mo fence="false" stretchy="false">}</mo>
<mo stretchy="false">)</mo>
<mo>∪<!-- ∪ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo class="MJX-variant">∖<!-- ∖ --></mo>
<mo fence="false" stretchy="false">{</mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>L</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo fence="false" stretchy="false">}</mo>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/6962089a62673ee5348bd8998a3642ae43593b50.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.193ex; height:3.509ex;" alt="{\displaystyle C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})}" loading="lazy"></span>
</p><p>Es darf immer nur <b>genau ein</b> Literal resolviert werden. Je nach Ausgangsklauseln ist die Bildung verschiedener Resolventen möglich.
</p><p>Anders notiert: Aus
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∧<!-- ∧ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle (A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/8083cc869ba386a8ba6c302062c2c36b6c4bda52.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:51.705ex; height:2.843ex;" alt="{\displaystyle (A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})}" loading="lazy"></span></dd></dl>
<p>wird auf die Resolvente
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A_{2}\vee \dots \vee A_{n}\vee B_{1}\vee \dots \vee B_{m}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle A_{2}\vee \dots \vee A_{n}\vee B_{1}\vee \dots \vee B_{m}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/0e2148c2bdba280c6c18b552dacf89ad151f27b7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:30.376ex; height:2.509ex;" alt="{\displaystyle A_{2}\vee \dots \vee A_{n}\vee B_{1}\vee \dots \vee B_{m}}" loading="lazy"></span></dd></dl>
<p>geschlossen.
</p><p>Die Resolvente ist <i>nicht äquivalent</i> zu den Ausgangsklauseln. Die Bedeutung der Resolvente liegt vielmehr darin, dass die Ausgangsklauseln nur dann <i>beide gleichzeitig erfüllbar</i> sind, wenn auch die Resolvente erfüllbar ist (<a href="Notwendige_Bedingung" class="mw-redirect" title="Notwendige Bedingung">notwendige Bedingung</a>). Gelingt es, die leere Klausel zu resolvieren, die stets unerfüllbar ist, ist somit die Unerfüllbarkeit der gesamten Formel gezeigt.
</p>
<div class="mw-heading mw-heading3"><h3 id="Beweis">Beweis</h3></div>
<p>Die Resolvente <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{R}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{R}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/05366cec35ae08b2e88c7c1ce8dcba451d837959.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.141ex; height:2.509ex;" alt="{\displaystyle C_{R}}" loading="lazy"></span> ist eine <a href="Notwendige_Bedingung" class="mw-redirect" title="Notwendige Bedingung">notwendige Bedingung</a> für die Ausgangsklauseln <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/babf569931f1a7b5182b9bec51873c2f5692fbb8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{1}}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/7ec545f7870665e1028b7492746848d149878808.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{2}}" loading="lazy"></span>, es gilt also
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (C_{1}\wedge C_{2})\rightarrow C_{R}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle (C_{1}\wedge C_{2})\rightarrow C_{R}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/792a6b620704d2060e1a9a0e7749a05469f7967b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.579ex; height:2.843ex;" alt="{\displaystyle (C_{1}\wedge C_{2})\rightarrow C_{R}}" loading="lazy"></span>.</dd></dl>
<p>Man sagt <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{R}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{R}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/05366cec35ae08b2e88c7c1ce8dcba451d837959.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.141ex; height:2.509ex;" alt="{\displaystyle C_{R}}" loading="lazy"></span> folgt aus <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/babf569931f1a7b5182b9bec51873c2f5692fbb8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{1}}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/7ec545f7870665e1028b7492746848d149878808.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.716ex; height:2.509ex;" alt="{\displaystyle C_{2}}" loading="lazy"></span>. Der Beweis zur Korrektheit dieser Resolution kann wie folgt geführt werden:
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}&amp;[(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\rightarrow (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv \neg [(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv (\neg A_{1}\wedge \neg A_{2}\wedge \dots \wedge \neg A_{n})\vee (\neg B_{1}\wedge \neg B_{2}\wedge \dots \wedge \neg B_{m}\wedge A_{1})\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv (\neg A_{1}\vee A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (A_{1}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv \neg A_{1}\vee A_{1}\\&amp;\equiv 1\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd></mtd>
<mtd>
<mi></mi>
<mo stretchy="false">[</mo>
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∧<!-- ∧ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo stretchy="false">]</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>3</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi></mi>
<mo>≡<!-- ≡ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mo stretchy="false">[</mo>
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∧<!-- ∧ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo stretchy="false">]</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>3</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi></mi>
<mo>≡<!-- ≡ --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∧<!-- ∧ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∧<!-- ∧ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>3</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi></mi>
<mo>≡<!-- ≡ --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>3</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>B</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi></mi>
<mo>≡<!-- ≡ --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<msub>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi></mi>
<mo>≡<!-- ≡ --></mo>
<mn>1</mn>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}&amp;[(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\rightarrow (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv \neg [(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv (\neg A_{1}\wedge \neg A_{2}\wedge \dots \wedge \neg A_{n})\vee (\neg B_{1}\wedge \neg B_{2}\wedge \dots \wedge \neg B_{m}\wedge A_{1})\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv (\neg A_{1}\vee A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (A_{1}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv \neg A_{1}\vee A_{1}\\&amp;\equiv 1\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/77a6ae79ab9d851641a5afbfd39d2dd926dacbfb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -8.671ex; width:110.664ex; height:18.509ex;" alt="{\displaystyle {\begin{aligned}&amp;[(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\rightarrow (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv \neg [(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv (\neg A_{1}\wedge \neg A_{2}\wedge \dots \wedge \neg A_{n})\vee (\neg B_{1}\wedge \neg B_{2}\wedge \dots \wedge \neg B_{m}\wedge A_{1})\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv (\neg A_{1}\vee A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (A_{1}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&amp;\equiv \neg A_{1}\vee A_{1}\\&amp;\equiv 1\end{aligned}}}" loading="lazy"></span></dd></dl>
<div class="mw-heading mw-heading3"><h3 id="Res-Operator">Res-Operator</h3></div>
<p>Das Ausführen eines einzelnen Resolutionsschrittes wird mit dem Res-Operator notiert:
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {Res} (F)=F\cup \{R\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>Res</mi>
<mo>⁡<!-- ⁡ --></mo>
<mo stretchy="false">(</mo>
<mi>F</mi>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mi>F</mi>
<mo>∪<!-- ∪ --></mo>
<mo fence="false" stretchy="false">{</mo>
<mi>R</mi>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \operatorname {Res} (F)=F\cup \{R\}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c3d39c493db1faf7658fba472040cb386eacace9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.72ex; height:2.843ex;" alt="{\displaystyle \operatorname {Res} (F)=F\cup \{R\}}" loading="lazy"></span>, wobei <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>R</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle R}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/4b0bfb3769bf24d80e15374dc37b0441e2616e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}" loading="lazy"></span> eine Resolvente zweier Klauseln aus <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>F</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle F}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"></span> ist</dd></dl>
<p>Mit <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {Res} ^{\star }(F)=\bigcup _{n\in \mathbb {N} }\operatorname {Res} ^{n}(F)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>Res</mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>⋆<!-- ⋆ --></mo>
</mrow>
</msup>
<mo>⁡<!-- ⁡ --></mo>
<mo stretchy="false">(</mo>
<mi>F</mi>
<mo stretchy="false">)</mo>
<mo>=</mo>
<munder>
<mo>⋃<!-- ⋃ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
<mo>∈<!-- ∈ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mi mathvariant="double-struck">N</mi>
</mrow>
</mrow>
</munder>
<msup>
<mi>Res</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msup>
<mo>⁡<!-- ⁡ --></mo>
<mo stretchy="false">(</mo>
<mi>F</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \operatorname {Res} ^{\star }(F)=\bigcup _{n\in \mathbb {N} }\operatorname {Res} ^{n}(F)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d73640776ea21972baddd5776d4c15ee0c573c83.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.171ex; width:23.446ex; height:5.676ex;" alt="{\displaystyle \operatorname {Res} ^{\star }(F)=\bigcup _{n\in \mathbb {N} }\operatorname {Res} ^{n}(F)}" loading="lazy"></span> bezeichnet man die Vereinigung aller möglichen Resolutionsschritte auf <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>F</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle F}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"></span>.
</p><p>Somit sind folgende Aussagen möglich:
</p>
<ol><li>ist die leere Klausel Element von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {Res} ^{\star }(F)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>Res</mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>⋆<!-- ⋆ --></mo>
</mrow>
</msup>
<mo>⁡<!-- ⁡ --></mo>
<mo stretchy="false">(</mo>
<mi>F</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \operatorname {Res} ^{\star }(F)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/44b6918aa5ae3933ebd358a608c04fcf6e33ef39.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.264ex; height:2.843ex;" alt="{\displaystyle \operatorname {Res} ^{\star }(F)}" loading="lazy"></span>, ist <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>F</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle F}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"></span> unerfüllbar und</li>
<li>ist die leere Klausel Element von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {Res} ^{\star }(\neg F)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>Res</mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>⋆<!-- ⋆ --></mo>
</mrow>
</msup>
<mo>⁡<!-- ⁡ --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>F</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \operatorname {Res} ^{\star }(\neg F)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/257846318dd6df0042826547c86a8191c91c20cf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.814ex; height:2.843ex;" alt="{\displaystyle \operatorname {Res} ^{\star }(\neg F)}" loading="lazy"></span>, ist <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>F</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle F}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"></span> eine <a href="Tautologie_(Logik)" title="Tautologie (Logik)">Tautologie</a></li></ol>
<div class="mw-heading mw-heading2"><h2 id="Resolution_und_Prädikatenlogik"><span id="Resolution_und_Pr.C3.A4dikatenlogik"></span>Resolution und Prädikatenlogik</h2></div>
<div class="mw-heading mw-heading3"><h3 id="Problemstellung">Problemstellung</h3></div>
<p>Für interessantere Problemstellungen ist das Instrumentarium der Aussagenlogik nicht ausreichend. Das Prinzip der Resolution sollte von der einfachen Aussagenlogik auf die <a href="Pr%C3%A4dikatenlogik" title="Prädikatenlogik">Prädikatenlogik</a> erster Stufe ausgeweitet werden können. Neben logischen Literalen sind dabei zu berücksichtigen:
</p>
<ul><li><i><a href="Variable_(Logik)" title="Variable (Logik)">Variablen</a></i> (beispielsweise Zahlenvariablen), üblicherweise mit Symbolen wie <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>x</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle x}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>y</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle y}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy"></span> bezeichnet</li>
<li>die <i><a href="Quantor" title="Quantor">Quantoren</a></i> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">∃<!-- ∃ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \exists }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/77ed842b6b90b2fdd825320cf8e5265fa937b583.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \exists }" loading="lazy"></span> (<i>der Existenzquantor</i>) und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">∀<!-- ∀ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \forall }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/bfc1a1a9c4c0f8d5df989c98aa2773ed657c5937.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \forall }" loading="lazy"></span> (<i>der Allquantor</i>),</li>
<li><i><a href="Konstante_(Logik)" title="Konstante (Logik)">Konstanten</a></i>, beispielsweise <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0,1,\pi \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mn>0</mn>
<mo>,</mo>
<mn>1</mn>
<mo>,</mo>
<mi>π<!-- π --></mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle 0,1,\pi \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/a3f5113578834259cf8910250f901d2ac90f4a08.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.112ex; height:2.509ex;" alt="{\displaystyle 0,1,\pi \,}" loading="lazy"></span></li>
<li>ein- und mehrwertige <i><a href="Funktion_(Mathematik)" title="Funktion (Mathematik)">Funktionen</a></i>, üblicherweise mit Symbolen wie <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f(x)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle f(x)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/202945cce41ecebb6f643f31d119c514bec7a074.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.418ex; height:2.843ex;" alt="{\displaystyle f(x)}" loading="lazy"></span> oder <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g(x,y)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>g</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo>,</mo>
<mi>y</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle g(x,y)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/bf358a54b0375e22ae5f3ab2c3e1a22c0c87e11c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.444ex; height:2.843ex;" alt="{\displaystyle g(x,y)}" loading="lazy"></span> bezeichnet.</li></ul>
<p>Ein durchaus typisches Beispiel für eine prädikatenlogische Aussage ist:
</p>
<table cellpadding="15">

<tbody><tr valign="top">
<td><b>1)</b>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x\exists y\forall zK(g(a,z),y)\implies K(g(f(a),f(z)),x)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">∀<!-- ∀ --></mi>
<mi>x</mi>
<mi mathvariant="normal">∃<!-- ∃ --></mi>
<mi>y</mi>
<mi mathvariant="normal">∀<!-- ∀ --></mi>
<mi>z</mi>
<mi>K</mi>
<mo stretchy="false">(</mo>
<mi>g</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo>,</mo>
<mi>z</mi>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi>y</mi>
<mo stretchy="false">)</mo>
<mspace width="thickmathspace"></mspace>
<mo stretchy="false">⟹<!-- ⟹ --></mo>
<mspace width="thickmathspace"></mspace>
<mi>K</mi>
<mo stretchy="false">(</mo>
<mi>g</mi>
<mo stretchy="false">(</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>z</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \forall x\exists y\forall zK(g(a,z),y)\implies K(g(f(a),f(z)),x)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/84890e9def279ad4c9a0d0dc4fc197e0c1779bba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:44.871ex; height:2.843ex;" alt="{\displaystyle \forall x\exists y\forall zK(g(a,z),y)\implies K(g(f(a),f(z)),x)}" loading="lazy"></span>
</td></tr></tbody></table>
<p>(Anmerkung: Setzen wir <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g(t,u)=\vert t-u\vert \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>g</mi>
<mo stretchy="false">(</mo>
<mi>t</mi>
<mo>,</mo>
<mi>u</mi>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mo fence="false" stretchy="false">|</mo>
<mi>t</mi>
<mo>−<!-- − --></mo>
<mi>u</mi>
<mo fence="false" stretchy="false">|</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle g(t,u)=\vert t-u\vert \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/563f32374f49fc93fd007eb06255f5d5e352cb79.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.917ex; height:2.843ex;" alt="{\displaystyle g(t,u)=\vert t-u\vert \,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle K(v,w)\equiv (v<w)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>K</mi>
<mo stretchy="false">(</mo>
<mi>v</mi>
<mo>,</mo>
<mi>w</mi>
<mo stretchy="false">)</mo>
<mo>≡<!-- ≡ --></mo>
<mo stretchy="false">(</mo>
<mi>v</mi>
<mo>&lt;</mo>
<mi>w</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle K(v,w)\equiv (v&lt;w)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f0ce30d76dd90ba07ff6674986f5d927a8855fe5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.886ex; height:2.843ex;" alt="{\displaystyle K(v,w)\equiv (v<w)\,}" loading="lazy"></span>, so liefert uns die obige Formel die formal-logische Definition der <a href="Stetige_Funktion" title="Stetige Funktion">Stetigkeit</a> der Funktion <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>f</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle f\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/ba5397b34cab7d96daac496a937b0c0fa076dff7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.666ex; height:2.509ex;" alt="{\displaystyle f\,}" loading="lazy"></span> im Punkt <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>a</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle a\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1d73aa5354c24942dab5316be466465a9d171510.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.617ex; height:1.676ex;" alt="{\displaystyle a\,}" loading="lazy"></span>.)
</p><p>Damit auf solche Aussagen die Resolution angewendet werden kann, müssen sie umgeformt und das oben beschriebene Verfahren erweitert werden.
</p>
<div class="mw-heading mw-heading3"><h3 id="Normalisierung">Normalisierung</h3></div>
<p>Die ersten Schritte bestehen darin, die zu widerlegende Aussage in eine Form zu bringen, die der konjunktiven Normalform der Aussagenlogik ähnelt.
</p>
<ol><li>Man bringt die zu widerlegende Formel in die <a href="Pr%C3%A4nexform" title="Pränexform">Pränexform</a>. Nach dieser Umformung stehen die Quantoren alle am Anfang der Formel, und der Rest der Formel hat die Gestalt einer konjunktiven Normalform.</li>
<li>Durch die Anwendung von <i>Skolemfunktionen</i> eliminiert man alle Existenzquantoren <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">∃<!-- ∃ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \exists }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/77ed842b6b90b2fdd825320cf8e5265fa937b583.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \exists }" loading="lazy"></span> aus der Formel und bringt sie in die <a href="Skolemform" title="Skolemform">Skolemform</a>.</li>
<li>Nun sind alle Variablen in der Funktion an Allquantoren <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">∀<!-- ∀ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \forall }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/bfc1a1a9c4c0f8d5df989c98aa2773ed657c5937.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \forall }" loading="lazy"></span> gebunden. Trifft man die Übereinkunft, Konstanten und Variablen unterschiedlich zu bezeichnen, beispielsweise Konstanten mit <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a,b,c,a_{1},a_{2},a_{3},\dotsc \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>a</mi>
<mo>,</mo>
<mi>b</mi>
<mo>,</mo>
<mi>c</mi>
<mo>,</mo>
<msub>
<mi>a</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>a</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>a</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>3</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle a,b,c,a_{1},a_{2},a_{3},\dotsc \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c98a2230044a942ee228cdf51f39c662c0849c4e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:19.4ex; height:2.509ex;" alt="{\displaystyle a,b,c,a_{1},a_{2},a_{3},\dotsc \,}" loading="lazy"></span> und Variablen mit <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x,y,z,x_{1},x_{2},x_{3},\dotsc \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>x</mi>
<mo>,</mo>
<mi>y</mi>
<mo>,</mo>
<mi>z</mi>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>3</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle x,y,z,x_{1},x_{2},x_{3},\dotsc \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f5a4f0aa156e0b3d99145b067389a199ffcc712f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.039ex; height:2.009ex;" alt="{\displaystyle x,y,z,x_{1},x_{2},x_{3},\dotsc \,}" loading="lazy"></span>, dann kann auch auf die explizite Notation des Allquantors verzichtet werden. Man lässt ihn ebenfalls weg und erhält die <a href="Klauselform" class="mw-redirect" title="Klauselform">Klauselform</a> der Aussage.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup></li></ol>
<p>Beispielsweise lautet die Klauselform der Formel <b>1)</b> aus dem vorigen Abschnitt:
</p>
<table cellpadding="15">

<tbody><tr valign="top">
<td><b>2)</b>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg K(g(a,z),s(x))\vee K(g(f(a),f(z)),x)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>K</mi>
<mo stretchy="false">(</mo>
<mi>g</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo>,</mo>
<mi>z</mi>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi>s</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mi>K</mi>
<mo stretchy="false">(</mo>
<mi>g</mi>
<mo stretchy="false">(</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>z</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \neg K(g(a,z),s(x))\vee K(g(f(a),f(z)),x)}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/199a77f7152d59b28878864708892cb0526fb3cc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:38.241ex; height:2.843ex;" alt="{\displaystyle \neg K(g(a,z),s(x))\vee K(g(f(a),f(z)),x)}" loading="lazy"></span>
</td></tr></tbody></table>
<div class="mw-heading mw-heading3"><h3 id="Substitution_und_Vereinheitlichung">Substitution und Vereinheitlichung</h3></div>
<p>Die Formeln
</p>
<table cellpadding="15">

<tbody><tr valign="top">
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(x)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(x)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/eaeeb92f3ec9c26cbd3d13b89daa47841ce49023.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.272ex; height:2.843ex;" alt="{\displaystyle P(x)\,}" loading="lazy"></span>
</td>
<td>und
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg P(a)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \neg P(a)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/e40fbefc4a0d7ba69bb6440b8581907c64b97302.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.722ex; height:2.843ex;" alt="{\displaystyle \neg P(a)\,}" loading="lazy"></span>
</td></tr></tbody></table>
<p>scheinen auf den ersten Blick nicht resolvierbar zu sein, da sie sich in <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>x</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle x\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/ab34739435d9d9d99cddf4041740b107343b1398.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.717ex; height:1.676ex;" alt="{\displaystyle x\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>a</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle a\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1d73aa5354c24942dab5316be466465a9d171510.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.617ex; height:1.676ex;" alt="{\displaystyle a\,}" loading="lazy"></span> unterscheiden. Da die freie Variable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>x</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle x\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/ab34739435d9d9d99cddf4041740b107343b1398.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.717ex; height:1.676ex;" alt="{\displaystyle x\,}" loading="lazy"></span> jedoch implizit ein Stellvertreter für alle <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>x</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle x\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/ab34739435d9d9d99cddf4041740b107343b1398.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.717ex; height:1.676ex;" alt="{\displaystyle x\,}" loading="lazy"></span> ist, darf (unter anderem) <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>a</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle a\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1d73aa5354c24942dab5316be466465a9d171510.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.617ex; height:1.676ex;" alt="{\displaystyle a\,}" loading="lazy"></span> für <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>x</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle x\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/ab34739435d9d9d99cddf4041740b107343b1398.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.717ex; height:1.676ex;" alt="{\displaystyle x\,}" loading="lazy"></span> eingesetzt werden.
</p><p>Man erhält also die beiden Terme
</p>
<table cellpadding="15">

<tbody><tr valign="top">
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(a)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(a)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/5b00eed4ae4df83297a2e4d1536966ec6d5a3a3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.172ex; height:2.843ex;" alt="{\displaystyle P(a)\,}" loading="lazy"></span>
</td>
<td>und
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg P(a)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \neg P(a)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/e40fbefc4a0d7ba69bb6440b8581907c64b97302.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.722ex; height:2.843ex;" alt="{\displaystyle \neg P(a)\,}" loading="lazy"></span>
</td></tr></tbody></table>
<p>die sich offensichtlich miteinander resolvieren lassen.
</p><p>Folgende Ersetzungen sind möglich:
</p>
<table cellpadding="15">

<tbody><tr valign="top">
<td><b>3a)</b>
</td>
<td>Ersetze Variable durch Konstante:
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(x)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(x)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/eaeeb92f3ec9c26cbd3d13b89daa47841ce49023.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.272ex; height:2.843ex;" alt="{\displaystyle P(x)\,}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rightarrow }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">→<!-- → --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \rightarrow }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/53e574cc3aa5b4bf5f3f5906caf121a378eef08b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \rightarrow }" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(a)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(a)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/5b00eed4ae4df83297a2e4d1536966ec6d5a3a3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.172ex; height:2.843ex;" alt="{\displaystyle P(a)\,}" loading="lazy"></span>
</td></tr>
<tr valign="top">
<td><b>3b)</b>
</td>
<td>Ersetze Variable durch eine andere Variable:
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(x)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(x)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/eaeeb92f3ec9c26cbd3d13b89daa47841ce49023.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.272ex; height:2.843ex;" alt="{\displaystyle P(x)\,}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rightarrow }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">→<!-- → --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \rightarrow }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/53e574cc3aa5b4bf5f3f5906caf121a378eef08b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \rightarrow }" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(y)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>y</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(y)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/990662417b334b73c171111a42f782d13bf39fc2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.097ex; height:2.843ex;" alt="{\displaystyle P(y)\,}" loading="lazy"></span>
</td></tr>
<tr valign="top">
<td><b>3c)</b>
</td>
<td>Ersetze Variable durch Funktion einer Variablen:
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(x)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(x)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/eaeeb92f3ec9c26cbd3d13b89daa47841ce49023.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.272ex; height:2.843ex;" alt="{\displaystyle P(x)\,}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rightarrow }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">→<!-- → --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \rightarrow }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/53e574cc3aa5b4bf5f3f5906caf121a378eef08b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \rightarrow }" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(f(y))\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>y</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(f(y))\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/b5c299807ae2dd836e0fbc370180553e734a5b7b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.185ex; height:2.843ex;" alt="{\displaystyle P(f(y))\,}" loading="lazy"></span>
</td></tr></tbody></table>
<p>Die Ersetzung von Variablen in einem Literal muss in konsistenter Weise durchgeführt werden: Wird eine Variable an einer Stelle durch einen Term ersetzt, so muss dies innerhalb des Literals überall geschehen:
</p>
<table cellpadding="15">

<tbody><tr valign="top">
<td><b>4a)</b>
</td>
<td>Korrekte Ersetzung:
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(x,f(x))\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo>,</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(x,f(x))\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1dbd4452b8685075edd5bfe416fa2afb472a0e9d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.723ex; height:2.843ex;" alt="{\displaystyle P(x,f(x))\,}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rightarrow }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">→<!-- → --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \rightarrow }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/53e574cc3aa5b4bf5f3f5906caf121a378eef08b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \rightarrow }" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(a,f(a))\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo>,</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(a,f(a))\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/3b3b9cda8b23370e6a56058ea1d1890c6b478192.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.523ex; height:2.843ex;" alt="{\displaystyle P(a,f(a))\,}" loading="lazy"></span>
</td></tr>
<tr valign="top">
<td><b>4b)</b>
</td>
<td>Verbotene Ersetzung:
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(x,f(x))\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo>,</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(x,f(x))\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1dbd4452b8685075edd5bfe416fa2afb472a0e9d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.723ex; height:2.843ex;" alt="{\displaystyle P(x,f(x))\,}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \nrightarrow }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo>↛<!-- ↛ --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \nrightarrow }</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/4c458d67617e028ed10948d2dbcfef80e9e060a2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.137ex; margin-bottom: -0.308ex; width:2.324ex; height:1.509ex;" alt="{\displaystyle \nrightarrow }" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(a,f(x))\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo>,</mo>
<mi>f</mi>
<mo stretchy="false">(</mo>
<mi>x</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(a,f(x))\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/93ce73af1b947ff51a4ff325bc3919ac2d9a4508.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.623ex; height:2.843ex;" alt="{\displaystyle P(a,f(x))\,}" loading="lazy"></span>
</td></tr></tbody></table>
<p>Sei <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lbrace x_{1},x_{2},\dotsc ,x_{n}\rbrace \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">{</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \lbrace x_{1},x_{2},\dotsc ,x_{n}\rbrace \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c8e2823be598f336d27d7269e594dfdc737a6a64.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.24ex; height:2.843ex;" alt="{\displaystyle \lbrace x_{1},x_{2},\dotsc ,x_{n}\rbrace \,}" loading="lazy"></span> eine Menge von Variablen. Sei <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lbrace t_{1},t_{2},\dotsc ,t_{n}\rbrace \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">{</mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \lbrace t_{1},t_{2},\dotsc ,t_{n}\rbrace \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/7c7e52e92f2bdd5132f8dacb49f69e7245a53137.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.77ex; height:2.843ex;" alt="{\displaystyle \lbrace t_{1},t_{2},\dotsc ,t_{n}\rbrace \,}" loading="lazy"></span> eine Menge von Termen, die aus Funktionen, Variablen oder Konstanten zusammengesetzt sein können.
</p>
<ul><li>Ein System <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/933054f2b86e79da95030b113a7c7dfdff643268.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.886ex; height:2.176ex;" alt="{\displaystyle S\,}" loading="lazy"></span> von Ersetzungen <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lbrace x_{1}\rightarrow t_{1},x_{2}\rightarrow t_{2},\dotsc ,x_{n}\rightarrow t_{n}\rbrace \,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">{</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">→<!-- → --></mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo stretchy="false">→<!-- → --></mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>x</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">→<!-- → --></mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \lbrace x_{1}\rightarrow t_{1},x_{2}\rightarrow t_{2},\dotsc ,x_{n}\rightarrow t_{n}\rbrace \,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c7bfd48604ec6b8c04f05c69bb962c54b7af08c8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:32.928ex; height:2.843ex;" alt="{\displaystyle \lbrace x_{1}\rightarrow t_{1},x_{2}\rightarrow t_{2},\dotsc ,x_{n}\rightarrow t_{n}\rbrace \,}" loading="lazy"></span> heißt eine <i>Substitution</i>.</li></ul>
<p>Seien <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}=P(t_{1},t_{2},\dotsc ,t_{n}),L_{2}=P(u_{1},u_{2},\dotsc ,u_{n}),\dotsc ,L_{m}=P(v_{1},v_{2},\dotsc ,v_{n})\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>=</mo>
<mi>P</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>,</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>=</mo>
<mi>P</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>u</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>u</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>u</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo>=</mo>
<mi>P</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>v</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>v</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>v</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}=P(t_{1},t_{2},\dotsc ,t_{n}),L_{2}=P(u_{1},u_{2},\dotsc ,u_{n}),\dotsc ,L_{m}=P(v_{1},v_{2},\dotsc ,v_{n})\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/fe0e6d00461151abdf9c74e0bf389403a5e2f3c1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:73.599ex; height:2.843ex;" alt="{\displaystyle L_{1}=P(t_{1},t_{2},\dotsc ,t_{n}),L_{2}=P(u_{1},u_{2},\dotsc ,u_{n}),\dotsc ,L_{m}=P(v_{1},v_{2},\dotsc ,v_{n})\,}" loading="lazy"></span> Literale über demselben Prädikat <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f60e07ebc2aadee94e4cbbccef71fd9bcf44f5f9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.133ex; height:2.176ex;" alt="{\displaystyle P\,}" loading="lazy"></span>, wobei die <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t_{i},u_{i},\dotsc ,v_{i}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>t</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>i</mi>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>u</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>i</mi>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>v</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>i</mi>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle t_{i},u_{i},\dotsc ,v_{i}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/81d3ced3df75f551d8dc27616e3c25e62da13883.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:12.295ex; height:2.343ex;" alt="{\displaystyle t_{i},u_{i},\dotsc ,v_{i}\,}" loading="lazy"></span> wiederum Terme sind.
</p>
<ul><li>Eine Substitution <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/933054f2b86e79da95030b113a7c7dfdff643268.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.886ex; height:2.176ex;" alt="{\displaystyle S\,}" loading="lazy"></span> heißt eine <i>Vereinheitlichung</i> (oder auch Unifikator) von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1},L_{2},\dotsc ,L_{m}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1},L_{2},\dotsc ,L_{m}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/2bb54c87b391d7e7cd0189a886bed498334fa0f1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:15.131ex; height:2.509ex;" alt="{\displaystyle L_{1},L_{2},\dotsc ,L_{m}\,}" loading="lazy"></span>, wenn durch die Anwendung von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/933054f2b86e79da95030b113a7c7dfdff643268.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.886ex; height:2.176ex;" alt="{\displaystyle S\,}" loading="lazy"></span> die Argumente aller Literale zur Übereinstimmung gebracht werden, das heißt, wenn <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S(L_{1})=S(L_{2})=\dotsb =S(L_{m})\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mi>S</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mo>⋯<!-- ⋯ --></mo>
<mo>=</mo>
<mi>S</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>m</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S(L_{1})=S(L_{2})=\dotsb =S(L_{m})\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/a5793dc0e569801c61f0327df57b0b25268e2b5e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.863ex; height:2.843ex;" alt="{\displaystyle S(L_{1})=S(L_{2})=\dotsb =S(L_{m})\,}" loading="lazy"></span>.</li></ul>
<p>Zwei Literale über demselben Prädikat haben nicht notwendigerweise eine Vereinheitlichung. Beispielsweise lassen sich <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(a)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>a</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(a)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/5b00eed4ae4df83297a2e4d1536966ec6d5a3a3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.172ex; height:2.843ex;" alt="{\displaystyle P(a)\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(b)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>P</mi>
<mo stretchy="false">(</mo>
<mi>b</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle P(b)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/6f35cb93be52ac593d2884770152c0a653646501.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.939ex; height:2.843ex;" alt="{\displaystyle P(b)\,}" loading="lazy"></span> nicht vereinheitlichen, wenn <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>a</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle a\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1d73aa5354c24942dab5316be466465a9d171510.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.617ex; height:1.676ex;" alt="{\displaystyle a\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>b</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle b\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/4b1bcf19f4ec75b1d2cc0be001e58a314fb0a940.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.385ex; height:2.176ex;" alt="{\displaystyle b\,}" loading="lazy"></span> unterschiedliche Konstanten sind.
</p>
<ul><li>Eine Vereinheitlichung <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/933054f2b86e79da95030b113a7c7dfdff643268.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.886ex; height:2.176ex;" alt="{\displaystyle S\,}" loading="lazy"></span> von Literalen heißt <i>allgemeinste Vereinheitlichung</i>, wenn es für jede andere Vereinheitlichung <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>T</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle T\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/476a8389064c06ab89963a2467aef525838da0cf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.023ex; height:2.176ex;" alt="{\displaystyle T\,}" loading="lazy"></span> dieser Literale eine Substitution <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle V\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>V</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle V\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f7ee72790178407e3a145dec860bb78a56672b10.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.174ex; height:2.176ex;" alt="{\displaystyle V\,}" loading="lazy"></span> gibt, so dass <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T=S\circ V\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>T</mi>
<mo>=</mo>
<mi>S</mi>
<mo>∘<!-- ∘ --></mo>
<mi>V</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle T=S\circ V\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/353be0c51354b0870734a52f22e0d343ba737c97.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.603ex; height:2.176ex;" alt="{\displaystyle T=S\circ V\,}" loading="lazy"></span>.</li></ul>
<p>Wenn eine Menge von Literalen eine Vereinheitlichung besitzt, dann besitzt sie eine allgemeinste Vereinheitlichung. Diese kann mit Hilfe eines relativ einfachen Algorithmus<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> ermittelt werden.
</p>
<div class="mw-heading mw-heading3"><h3 id="Resolution_prädikatenlogischer_Klauseln"><span id="Resolution_pr.C3.A4dikatenlogischer_Klauseln"></span>Resolution prädikatenlogischer Klauseln</h3></div>
<p>Mit diesem Instrumentarium kann das Resolutionsverfahren auf Aussagen der Prädikatenlogik ausgeweitet werden.
</p>
<ul><li>Seien <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1},C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1},C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c4d87342b0ee80da33355377e86d57006ae2219c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.853ex; height:2.509ex;" alt="{\displaystyle C_{1},C_{2}\,}" loading="lazy"></span> zwei Klauseln einer normalisierten prädikatenlogischen Aussage. <a href="Ohne_Beschr%C3%A4nkung_der_Allgemeinheit" title="Ohne Beschränkung der Allgemeinheit">Ohne Beschränkung der Allgemeinheit</a> darf vorausgesetzt werden, dass diese keine übereinstimmenden Variablen enthalten (da sie durch einen Allquantor gebunden sind, können wir gleichnamige Variablen in einer Klausel umbenennen, auch wenn der Allquantor nicht mehr explizit geschrieben wird).</li>
<li>Seien <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/4e4e19a1d357cd7bc605289a07211a1eae7006b7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.024ex; height:2.509ex;" alt="{\displaystyle L_{1}\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f01e29df8564946d59c325715d9adf1c9d7f3e9a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.024ex; height:2.509ex;" alt="{\displaystyle L_{2}\,}" loading="lazy"></span> positive bzw. negiert vorkommende Literale in <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> bzw. <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/40f3e757e084c7f6e4a02cc971dea82db704a97b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{2}\,}" loading="lazy"></span>, die eine allgemeinste Vereinheitlichung <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/933054f2b86e79da95030b113a7c7dfdff643268.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.886ex; height:2.176ex;" alt="{\displaystyle S\,}" loading="lazy"></span> besitzen.</li></ul>
<p>Dann heißt
</p>
<ul><li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{R}=S(C_{1}\cup C_{2})\setminus \{S(L_{1}),\neg S(L_{2})\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msub>
<mo>=</mo>
<mi>S</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∪<!-- ∪ --></mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo class="MJX-variant">∖<!-- ∖ --></mo>
<mo fence="false" stretchy="false">{</mo>
<mi>S</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>,</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>S</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{R}=S(C_{1}\cup C_{2})\setminus \{S(L_{1}),\neg S(L_{2})\}}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/6dc194a4e911567c060ee89adc2d9c71116e90cf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:36.558ex; height:2.843ex;" alt="{\displaystyle C_{R}=S(C_{1}\cup C_{2})\setminus \{S(L_{1}),\neg S(L_{2})\}}" loading="lazy"></span> ein <i>binärer Resolvent</i> von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/40f3e757e084c7f6e4a02cc971dea82db704a97b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{2}\,}" loading="lazy"></span>.</li>
<li>Sei ferner <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>C</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/785a192e3331793e37b1be0c5315d196da1a7049.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.153ex; height:2.176ex;" alt="{\displaystyle C\,}" loading="lazy"></span> eine Klausel mit einer Teilmenge von Literalen, die eine allgemeinste Vereinheitlichung <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/933054f2b86e79da95030b113a7c7dfdff643268.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.886ex; height:2.176ex;" alt="{\displaystyle S\,}" loading="lazy"></span> besitzt.</li></ul>
<p>Dann heißt
</p>
<ul><li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S(C)\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>S</mi>
<mo stretchy="false">(</mo>
<mi>C</mi>
<mo stretchy="false">)</mo>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle S(C)\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/7b52de116a013f28d97f8da1e627ae6c5429e85c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.462ex; height:2.843ex;" alt="{\displaystyle S(C)\,}" loading="lazy"></span> ein <i>Faktor</i> von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>C</mi>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/785a192e3331793e37b1be0c5315d196da1a7049.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.153ex; height:2.176ex;" alt="{\displaystyle C\,}" loading="lazy"></span>.</li></ul>
<p>Ein <i>Resolvent</i> zweier Klauseln <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1},C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1},C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c4d87342b0ee80da33355377e86d57006ae2219c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.853ex; height:2.509ex;" alt="{\displaystyle C_{1},C_{2}\,}" loading="lazy"></span> ist
</p>
<ul><li>entweder ein binärer Resolvent von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/40f3e757e084c7f6e4a02cc971dea82db704a97b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{2}\,}" loading="lazy"></span>.</li>
<li>oder ein binärer Resolvent von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> und einem Faktor von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/40f3e757e084c7f6e4a02cc971dea82db704a97b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{2}\,}" loading="lazy"></span>.</li>
<li>oder ein binärer Resolvent eines Faktors von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> und <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/40f3e757e084c7f6e4a02cc971dea82db704a97b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{2}\,}" loading="lazy"></span>.</li>
<li>oder ein binärer Resolvent eines Faktors von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> und eines Faktors von <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{2}\,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>C</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mspace width="thinmathspace"></mspace>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle C_{2}\,}</annotation>
</semantics>
</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/40f3e757e084c7f6e4a02cc971dea82db704a97b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{2}\,}" loading="lazy"></span>.</li></ul>
<p>Das Resolutionsverfahren für prädikatenlogische Aussagen besteht darin, so lange solche Resolventen zu erzeugen, bis die leere Klausel erzeugt und damit der Widerspruchsbeweis erbracht ist.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>
</p>
<div class="mw-heading mw-heading2"><h2 id="Beispiel">Beispiel</h2></div>
<div class="mw-heading mw-heading3"><h3 id="Ein_logisches_Rätsel"><span id="Ein_logisches_R.C3.A4tsel"></span>Ein logisches Rätsel</h3></div>
<p>Wir wollen das Prinzip am Beispiel eines kleinen, nicht wörtlich zu nehmenden logischen Rätsels illustrieren:
</p><p>Seit dem Altertum ist bekannt, dass alle Athener klug (1) und alle Spartaner heldenmütig (2) sind. Außerdem ist bekannt, dass ein profundes Misstrauen zwischen beiden Städten herrscht, so dass doppelte Stadtbürgerschaften ausgeschlossen sind (3). Unser nach Griechenland entsandter Forscher war neulich zu Gast bei einer Konferenz. Mit Ausnahme unseres Forschers stammte jeder der Anwesenden aus einer der beiden Städte (4).
</p><p>Der Forscher kam ins Gespräch mit den Herren Diogenes, Platon und Euklid. Mit ihren berühmten Vorbildern hatten diese nur den Namen gemein. Die Herren zogen kräftig übereinander vom Leder. Euklid sagte: „Wenn Platon Spartaner ist, dann ist Diogenes feige!“ (5) – Platon behauptete: „Diogenes ist eine Memme, wenn Euklid Spartaner ist!“ (6) „Wenn Diogenes allerdings Athener ist, dann ist Euklid ein Waschlappen!“ (7) – Worauf sich Diogenes den Bart glatt strich und postulierte: „Wenn Platon Athener ist, dann ist Euklid ein Dummkopf!“ (8)
</p><p>Bei aller Spitzzüngigkeit blieben die drei Herren mit ihren Behauptungen bei der Wahrheit. Wer kommt aus welcher Stadt?
</p>
<div class="mw-heading mw-heading3"><h3 id="Das_Rätsel_in_Klauselform"><span id="Das_R.C3.A4tsel_in_Klauselform"></span>Das Rätsel in Klauselform</h3></div>
<p>Wir setzen p für Platon, d für Diogenes, e für Euklid. Die Prädikate „ist Athener“, „ist Spartaner“, „ist heldenmütig“ und „ist klug“ bezeichnen wir mit A, S, H und K. Wir übersetzen die oben genannten Aussagen in die Klauselform und erhalten:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>¬A(x) v K(x)
</td>
<td>
</td>
<td>(1)
</td></tr>
<tr>
<td>¬S(x) v H(x)
</td>
<td>
</td>
<td>(2)
</td></tr>
<tr>
<td>¬A(x) v ¬S(x)
</td>
<td>
</td>
<td>(3)
</td></tr>
<tr>
<td>A(x) v S(x)
</td>
<td>
</td>
<td>(4)
</td></tr>
<tr>
<td>¬S(p) v ¬H(d)
</td>
<td>
</td>
<td>(5)
</td></tr>
<tr>
<td>¬S(e) v ¬H(d)
</td>
<td>
</td>
<td>(6)
</td></tr>
<tr>
<td>¬A(d) v ¬H(e)
</td>
<td>
</td>
<td>(7)
</td></tr>
<tr>
<td>¬A(p) v ¬K(e)
</td>
<td>
</td>
<td>(8)
</td></tr></tbody></table>
<div class="mw-heading mw-heading3"><h3 id="Die_Auflösung"><span id="Die_Aufl.C3.B6sung"></span>Die Auflösung</h3></div>
<p>Wir nehmen an, Platon sei Athener:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>A(p)
</td>
<td>{Annahme}
</td>
<td>(9)
</td></tr></tbody></table>
<p>Nun wenden wir das Resolutionsprinzip an und erhalten:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>¬K(e)
</td>
<td>{aus Resolution von (9) mit (8)}
</td>
<td>(10)
</td></tr>
<tr>
<td>¬A(e)
</td>
<td>{aus Substitution von e für x und Resolution (10,1)}
</td>
<td>(11)
</td></tr>
<tr>
<td>S(e)
</td>
<td>{Subs. (e:x), Res. (11,4)}
</td>
<td>(12)
</td></tr>
<tr>
<td>¬H(d)
</td>
<td>{Res. (12,6)}
</td>
<td>(13)
</td></tr>
<tr>
<td>¬S(d)
</td>
<td>{Subs. (d:x), Res. (13,2)}
</td>
<td>(14)
</td></tr>
<tr>
<td>A(d)
</td>
<td>{Subs. (d:x), Res. (14,4)}
</td>
<td>(15)
</td></tr>
<tr>
<td>¬H(e)
</td>
<td>{Res. (15,7)}
</td>
<td>(16)
</td></tr>
<tr>
<td>¬S(e)
</td>
<td>{Subs. (e:x), Res. (16,2)}
</td>
<td>(17)
</td></tr>
<tr>
<td>leere Klausel
</td>
<td>{Res. (17,12)}
</td>
<td>(18)
</td></tr></tbody></table>
<p>Somit ist die Annahme (9) zum Widerspruch geführt. Sie ist mitsamt den aus ihr abgeleiteten Klauseln (10) bis (18) zu verwerfen. Wir erhalten stattdessen:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>¬A(p)
</td>
<td>{da (9) falsch ist}
</td>
<td>(19)
</td></tr>
<tr>
<td>S(p)
</td>
<td>{Subs. (p:x), Res. (19,4)}
</td>
<td>(20)
</td></tr></tbody></table>
<p>Nehmen wir nun an, Diogenes sei Spartaner, und wenden wir weiterhin das Resolutionsprinzip an:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>S(d)
</td>
<td>{Annahme}
</td>
<td>(21)
</td></tr>
<tr>
<td>H(d)
</td>
<td>{Subs. (d:x), Res. (21,2)}
</td>
<td>(22)
</td></tr>
<tr>
<td>¬S(p)
</td>
<td>{Res. (22,5)}
</td>
<td>(23)
</td></tr>
<tr>
<td>leere Klausel
</td>
<td>{Res. (23,20)}
</td>
<td>(24)
</td></tr></tbody></table>
<p>Somit ist die Annahme (21) widerlegt und mitsamt den aus ihr abgeleiteten Klauseln (22) – (24) zu verwerfen. Wir erhalten stattdessen:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>¬S(d)
</td>
<td>{da (21) falsch ist}
</td>
<td>(25)
</td></tr>
<tr>
<td>A(d)
</td>
<td>{Subs. (d:x), Res. (25,4)}
</td>
<td>(26)
</td></tr></tbody></table>
<p>Nehmen wir an, Euklid sei Spartaner. Wir erhalten:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>S(e)
</td>
<td>{Annahme}
</td>
<td>(27)
</td></tr>
<tr>
<td>H(e)
</td>
<td>{Subs. (e:x), Res. (27, 2)}
</td>
<td>(28)
</td></tr>
<tr>
<td>¬A(d)
</td>
<td>{Res. (28, 7)}
</td>
<td>(29)
</td></tr>
<tr>
<td>leere Klausel
</td>
<td>{Res. (29,26)}
</td>
<td>(30)
</td></tr></tbody></table>
<p>Also ist (27) falsch und samt (28) – (30) zu verwerfen. Wir erhalten stattdessen:
</p>
<table>

<tbody><tr>
<th width="120">
</th>
<th width="450">
</th>
<th width="50">
</th></tr>
<tr>
<td>¬S(e)
</td>
<td>{da (27) falsch ist}
</td>
<td>(31)
</td></tr>
<tr>
<td>A(e)
</td>
<td>{Subs. (e:x), Res. (31,4)}
</td>
<td>(32)
</td></tr></tbody></table>
<p>Platon ist Spartaner (20). Diogenes ist Athener (26), ebenso Euklid (32).
</p>
<div class="mw-heading mw-heading2"><h2 id="Terminierung_und_Komplexität"><span id="Terminierung_und_Komplexit.C3.A4t"></span>Terminierung und Komplexität</h2></div>
<p>Im Falle der Aussagenlogik <a href="Terminiertheit" title="Terminiertheit">terminiert</a> das Verfahren: Es liefert in endlicher Zeit ein Ergebnis, ob eine vorgelegte Aussage erfüllbar ist. Die Rechenzeit wächst im allgemeinen Fall und mit den derzeit bekannten Verfahren exponentiell mit der Anzahl der Literale. Das Problem ist <a href="NP-Vollst%C3%A4ndigkeit" title="NP-Vollständigkeit">NP-vollständig</a>.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>
</p><p>Im Falle der Prädikatenlogik terminiert das Verfahren stets mit dem korrekten Ergebnis, wenn es auf eine unerfüllbare Formel angewendet wird. Bei einer erfüllbaren Formel kommt es jedoch vor, dass das Verfahren kein Ende findet. Man spricht von <a href="Semi-Entscheidbarkeit" class="mw-redirect" title="Semi-Entscheidbarkeit">Semi-Entscheidbarkeit</a>. Wäre es anders, dann wäre das Resolutionsverfahren ein Algorithmus, um prädikatenlogische Formeln allgemein zu entscheiden – was unmöglich ist, da das Gültigkeitsproblem in der Prädikatenlogik nicht <a href="Entscheidbarkeit" title="Entscheidbarkeit">entscheidbar</a> ist.
</p>
<div class="mw-heading mw-heading2"><h2 id="Andere_Kalküle_im_logischen_Einsatz"><span id="Andere_Kalk.C3.BCle_im_logischen_Einsatz"></span>Andere Kalküle im logischen Einsatz</h2></div>
<ul><li><a href="Baumkalk%C3%BCl" title="Baumkalkül">Baumkalkül</a>: in gewisser Weise unter den Kalkülen der nächste Verwandte des Resolutionskalküls</li>
<li><a href="Hilbert-Kalk%C3%BCl" title="Hilbert-Kalkül">axiomatische Kalküle</a></li>
<li><a href="Systeme_nat%C3%BCrlichen_Schlie%C3%9Fens" title="Systeme natürlichen Schließens">Systeme natürlichen Schließens</a></li>
<li><a href="Sequenzenkalk%C3%BCl" title="Sequenzenkalkül">Sequenzenkalkül</a></li>
<li><a href="Existential_Graphs" title="Existential Graphs">Existential Graphs</a></li></ul>
<div class="mw-heading mw-heading2"><h2 id="Quellen">Quellen</h2></div>
<ol class="references">
<li id="cite_note-1"><span class="mw-cite-backlink"><a href="#cite_ref-1">↑</a></span> <span class="reference-text">Davis, Martin: <i>Eliminating the Irrelevant from Mechanical Proofs.</i> in: <i>Journal of Symbolic Logic</i>, <span class="-print"><a href="Internationale_Standardnummer_f%C3%BCr_fortlaufende_Sammelwerke" title="Internationale Standardnummer für fortlaufende Sammelwerke">ISSN</a>&nbsp;<span style="white-space:nowrap"><a rel="nofollow" class="external text" href="https://zdb-katalog.de/list.xhtml?t=iss%3D%220022-4812%22&amp;key=cql">0022-4812</a></span></span>, Vol. 32, No. 1 (Mar., 1967), pp. 118–119</span>
</li>
<li id="cite_note-2"><span class="mw-cite-backlink"><a href="#cite_ref-2">↑</a></span> <span class="reference-text">Chang, Chin-Liang; Lee, Richard Char-Tung: <i>Symbolic Logic and Mechanical Theorem Proving</i>, Academic Press, 1973, ISBN 0-12-170350-9, S. 77ff</span>
</li>
<li id="cite_note-3"><span class="mw-cite-backlink"><a href="#cite_ref-3">↑</a></span> <span class="reference-text">Chang, Chin-Liang; Lee, Richard Char-Tung: S<i>ymbolic Logic and Mechanical Theorem Proving</i>, Academic Press, 1973, ISBN 0-12-170350-9, S. 80–81</span>
</li>
<li id="cite_note-4"><span class="mw-cite-backlink"><a href="#cite_ref-4">↑</a></span> <span class="reference-text">Haken, A. "The Intractability of Resolution", Theoretical Computer Science 39 (1985), pp. 297–308.</span>
</li>
</ol>
<div class="mw-heading mw-heading2"><h2 id="Literatur">Literatur</h2></div>
<ul><li>Chang, Chin-Liang; Lee, Richard Char-Tung: <i>Symbolic Logic and Mechanical Theorem Proving</i>, Academic Press, 1973, ISBN 0-12-170350-9</li></ul>
<div class="mw-heading mw-heading2"><h2 id="Weblinks">Weblinks</h2></div>
<ul><li><a rel="nofollow" class="external text" href="https://lecture2go.uni-hamburg.de/l2go/-/get/v/12155">Aussagenlogik -Resolution</a> Video der Vorlesung von Carola Eschenbach, 2011, Fachbereich Informatik, Universität Hamburg</li>
<li><a rel="nofollow" class="external text" href="https://formal.kastel.kit.edu/teaching/FormSysWS2425/FormSys.pdf">Formale Systeme, Kap. 5.3</a>, Vorlesungsskript von Peter H. Schmitt, 2016, <a href="KIT" class="mw-redirect" title="KIT">KIT</a> (PDF-Datei; 2,7 MB)</li>
<li><a class="external text" href="https://en.wikibooks.org/wiki/Logic_for_Computer_Scientists/Propositional_Logic/Resolution">Logic for Computer Scientists</a>, von <a href="Ulrich_Furbach" title="Ulrich Furbach">Ulrich Furbach</a>, Universität Koblenz-Landau</li>
<li><a rel="nofollow" class="external text" href="https://www.informatik.uni-hamburg.de/TGI/lehre/vl/WS1516/FGI3-Logik/Folien/fgi3_v2_handout.pdf">Aussagenlogik - Resolution</a> Vorlesungsskript von Frank Heitmann, 2015, Universität Hamburg</li></ul></div><!--htdig_noindex--><div><div class="zim-footer">
Dieser Artikel wurde von <a class="external text" title="Zuletzt bearbeitet am 2025-05-15" href="https://de.wikipedia.org/wiki/?title=Resolution_(Logik)&amp;oldid=256034601">Wikipedia</a> herausgegeben. Der Text ist unter <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.de">Creative Commons Attribution-Share Alike 4.0</a> verfügbar, sofern nicht anders angegeben. Für die Mediendateien können zusätzliche Bedingungen gelten.
</div>
</div><!--/htdig_noindex--></div>
</div>
</main>
</div>
</div>
</div>
<script src="./_webp_/webpHandler.js"></script>

</body></html>